0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 16 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 11 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 0 ms)
↳16 QDP
↳17 QDPSizeChangeProof (⇔, 0 ms)
↳18 YES
fib_in_ga(0, 0) → fib_out_ga(0, 0)
fib_in_ga(s(0), s(0)) → fib_out_ga(s(0), s(0))
fib_in_ga(s(s(X)), N) → U3_ga(X, N, fib_in_ga(s(X), N1))
U3_ga(X, N, fib_out_ga(s(X), N1)) → U4_ga(X, N, N1, fib_in_ga(X, N2))
U4_ga(X, N, N1, fib_out_ga(X, N2)) → U5_ga(X, N, add_in_gga(N1, N2, N))
add_in_gga(0, 0, 0) → add_out_gga(0, 0, 0)
add_in_gga(s(X), Y, s(N)) → U1_gga(X, Y, N, add_in_gga(X, Y, N))
add_in_gga(X, s(Y), s(N)) → U2_gga(X, Y, N, add_in_gga(X, Y, N))
U2_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(X, s(Y), s(N))
U1_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(s(X), Y, s(N))
U5_ga(X, N, add_out_gga(N1, N2, N)) → fib_out_ga(s(s(X)), N)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
fib_in_ga(0, 0) → fib_out_ga(0, 0)
fib_in_ga(s(0), s(0)) → fib_out_ga(s(0), s(0))
fib_in_ga(s(s(X)), N) → U3_ga(X, N, fib_in_ga(s(X), N1))
U3_ga(X, N, fib_out_ga(s(X), N1)) → U4_ga(X, N, N1, fib_in_ga(X, N2))
U4_ga(X, N, N1, fib_out_ga(X, N2)) → U5_ga(X, N, add_in_gga(N1, N2, N))
add_in_gga(0, 0, 0) → add_out_gga(0, 0, 0)
add_in_gga(s(X), Y, s(N)) → U1_gga(X, Y, N, add_in_gga(X, Y, N))
add_in_gga(X, s(Y), s(N)) → U2_gga(X, Y, N, add_in_gga(X, Y, N))
U2_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(X, s(Y), s(N))
U1_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(s(X), Y, s(N))
U5_ga(X, N, add_out_gga(N1, N2, N)) → fib_out_ga(s(s(X)), N)
FIB_IN_GA(s(s(X)), N) → U3_GA(X, N, fib_in_ga(s(X), N1))
FIB_IN_GA(s(s(X)), N) → FIB_IN_GA(s(X), N1)
U3_GA(X, N, fib_out_ga(s(X), N1)) → U4_GA(X, N, N1, fib_in_ga(X, N2))
U3_GA(X, N, fib_out_ga(s(X), N1)) → FIB_IN_GA(X, N2)
U4_GA(X, N, N1, fib_out_ga(X, N2)) → U5_GA(X, N, add_in_gga(N1, N2, N))
U4_GA(X, N, N1, fib_out_ga(X, N2)) → ADD_IN_GGA(N1, N2, N)
ADD_IN_GGA(s(X), Y, s(N)) → U1_GGA(X, Y, N, add_in_gga(X, Y, N))
ADD_IN_GGA(s(X), Y, s(N)) → ADD_IN_GGA(X, Y, N)
ADD_IN_GGA(X, s(Y), s(N)) → U2_GGA(X, Y, N, add_in_gga(X, Y, N))
ADD_IN_GGA(X, s(Y), s(N)) → ADD_IN_GGA(X, Y, N)
fib_in_ga(0, 0) → fib_out_ga(0, 0)
fib_in_ga(s(0), s(0)) → fib_out_ga(s(0), s(0))
fib_in_ga(s(s(X)), N) → U3_ga(X, N, fib_in_ga(s(X), N1))
U3_ga(X, N, fib_out_ga(s(X), N1)) → U4_ga(X, N, N1, fib_in_ga(X, N2))
U4_ga(X, N, N1, fib_out_ga(X, N2)) → U5_ga(X, N, add_in_gga(N1, N2, N))
add_in_gga(0, 0, 0) → add_out_gga(0, 0, 0)
add_in_gga(s(X), Y, s(N)) → U1_gga(X, Y, N, add_in_gga(X, Y, N))
add_in_gga(X, s(Y), s(N)) → U2_gga(X, Y, N, add_in_gga(X, Y, N))
U2_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(X, s(Y), s(N))
U1_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(s(X), Y, s(N))
U5_ga(X, N, add_out_gga(N1, N2, N)) → fib_out_ga(s(s(X)), N)
FIB_IN_GA(s(s(X)), N) → U3_GA(X, N, fib_in_ga(s(X), N1))
FIB_IN_GA(s(s(X)), N) → FIB_IN_GA(s(X), N1)
U3_GA(X, N, fib_out_ga(s(X), N1)) → U4_GA(X, N, N1, fib_in_ga(X, N2))
U3_GA(X, N, fib_out_ga(s(X), N1)) → FIB_IN_GA(X, N2)
U4_GA(X, N, N1, fib_out_ga(X, N2)) → U5_GA(X, N, add_in_gga(N1, N2, N))
U4_GA(X, N, N1, fib_out_ga(X, N2)) → ADD_IN_GGA(N1, N2, N)
ADD_IN_GGA(s(X), Y, s(N)) → U1_GGA(X, Y, N, add_in_gga(X, Y, N))
ADD_IN_GGA(s(X), Y, s(N)) → ADD_IN_GGA(X, Y, N)
ADD_IN_GGA(X, s(Y), s(N)) → U2_GGA(X, Y, N, add_in_gga(X, Y, N))
ADD_IN_GGA(X, s(Y), s(N)) → ADD_IN_GGA(X, Y, N)
fib_in_ga(0, 0) → fib_out_ga(0, 0)
fib_in_ga(s(0), s(0)) → fib_out_ga(s(0), s(0))
fib_in_ga(s(s(X)), N) → U3_ga(X, N, fib_in_ga(s(X), N1))
U3_ga(X, N, fib_out_ga(s(X), N1)) → U4_ga(X, N, N1, fib_in_ga(X, N2))
U4_ga(X, N, N1, fib_out_ga(X, N2)) → U5_ga(X, N, add_in_gga(N1, N2, N))
add_in_gga(0, 0, 0) → add_out_gga(0, 0, 0)
add_in_gga(s(X), Y, s(N)) → U1_gga(X, Y, N, add_in_gga(X, Y, N))
add_in_gga(X, s(Y), s(N)) → U2_gga(X, Y, N, add_in_gga(X, Y, N))
U2_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(X, s(Y), s(N))
U1_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(s(X), Y, s(N))
U5_ga(X, N, add_out_gga(N1, N2, N)) → fib_out_ga(s(s(X)), N)
ADD_IN_GGA(X, s(Y), s(N)) → ADD_IN_GGA(X, Y, N)
ADD_IN_GGA(s(X), Y, s(N)) → ADD_IN_GGA(X, Y, N)
fib_in_ga(0, 0) → fib_out_ga(0, 0)
fib_in_ga(s(0), s(0)) → fib_out_ga(s(0), s(0))
fib_in_ga(s(s(X)), N) → U3_ga(X, N, fib_in_ga(s(X), N1))
U3_ga(X, N, fib_out_ga(s(X), N1)) → U4_ga(X, N, N1, fib_in_ga(X, N2))
U4_ga(X, N, N1, fib_out_ga(X, N2)) → U5_ga(X, N, add_in_gga(N1, N2, N))
add_in_gga(0, 0, 0) → add_out_gga(0, 0, 0)
add_in_gga(s(X), Y, s(N)) → U1_gga(X, Y, N, add_in_gga(X, Y, N))
add_in_gga(X, s(Y), s(N)) → U2_gga(X, Y, N, add_in_gga(X, Y, N))
U2_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(X, s(Y), s(N))
U1_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(s(X), Y, s(N))
U5_ga(X, N, add_out_gga(N1, N2, N)) → fib_out_ga(s(s(X)), N)
ADD_IN_GGA(X, s(Y), s(N)) → ADD_IN_GGA(X, Y, N)
ADD_IN_GGA(s(X), Y, s(N)) → ADD_IN_GGA(X, Y, N)
ADD_IN_GGA(X, s(Y)) → ADD_IN_GGA(X, Y)
ADD_IN_GGA(s(X), Y) → ADD_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
U3_GA(X, N, fib_out_ga(s(X), N1)) → FIB_IN_GA(X, N2)
FIB_IN_GA(s(s(X)), N) → U3_GA(X, N, fib_in_ga(s(X), N1))
FIB_IN_GA(s(s(X)), N) → FIB_IN_GA(s(X), N1)
fib_in_ga(0, 0) → fib_out_ga(0, 0)
fib_in_ga(s(0), s(0)) → fib_out_ga(s(0), s(0))
fib_in_ga(s(s(X)), N) → U3_ga(X, N, fib_in_ga(s(X), N1))
U3_ga(X, N, fib_out_ga(s(X), N1)) → U4_ga(X, N, N1, fib_in_ga(X, N2))
U4_ga(X, N, N1, fib_out_ga(X, N2)) → U5_ga(X, N, add_in_gga(N1, N2, N))
add_in_gga(0, 0, 0) → add_out_gga(0, 0, 0)
add_in_gga(s(X), Y, s(N)) → U1_gga(X, Y, N, add_in_gga(X, Y, N))
add_in_gga(X, s(Y), s(N)) → U2_gga(X, Y, N, add_in_gga(X, Y, N))
U2_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(X, s(Y), s(N))
U1_gga(X, Y, N, add_out_gga(X, Y, N)) → add_out_gga(s(X), Y, s(N))
U5_ga(X, N, add_out_gga(N1, N2, N)) → fib_out_ga(s(s(X)), N)
U3_GA(X, fib_out_ga(N1)) → FIB_IN_GA(X)
FIB_IN_GA(s(s(X))) → U3_GA(X, fib_in_ga(s(X)))
FIB_IN_GA(s(s(X))) → FIB_IN_GA(s(X))
fib_in_ga(0) → fib_out_ga(0)
fib_in_ga(s(0)) → fib_out_ga(s(0))
fib_in_ga(s(s(X))) → U3_ga(X, fib_in_ga(s(X)))
U3_ga(X, fib_out_ga(N1)) → U4_ga(N1, fib_in_ga(X))
U4_ga(N1, fib_out_ga(N2)) → U5_ga(add_in_gga(N1, N2))
add_in_gga(0, 0) → add_out_gga(0)
add_in_gga(s(X), Y) → U1_gga(add_in_gga(X, Y))
add_in_gga(X, s(Y)) → U2_gga(add_in_gga(X, Y))
U2_gga(add_out_gga(N)) → add_out_gga(s(N))
U1_gga(add_out_gga(N)) → add_out_gga(s(N))
U5_ga(add_out_gga(N)) → fib_out_ga(N)
fib_in_ga(x0)
U3_ga(x0, x1)
U4_ga(x0, x1)
add_in_gga(x0, x1)
U2_gga(x0)
U1_gga(x0)
U5_ga(x0)
From the DPs we obtained the following set of size-change graphs: